SPIN model checker
Pour les articles homonymes, voir Spin (homonymie).
| Développé par | Gerard Holzmann |
|---|---|
| Première version | [1] |
| Dernière version | 6.5.2 ()[2] |
| Dépôt | github.com/nimble-code/Spin |
| Écrit en | C |
| Système d'exploitation | Linux, Microsoft Windows et macOS |
| Type | Model checking |
| Licence | BSD 3-clauses |
| Site web | spinroot.com |
SPIN est un outil général pour vérifier la correction de modèles logiciels concurrents de manière rigoureuse et généralement automatisée. Il a été écrit, à partir de 1980, par Gerard J. Holzmann et d'autres membres du groupe Unix du Computing Sciences Research Center des Bell Labs. Le logiciel est disponible gratuitement depuis 1991 et continue d'évoluer pour suivre le rythme des nouveaux développements dans ce domaine.
Description
[modifier | modifier le code]Les systèmes à vérifier sont décrits en langage Promela (abréviation pour Process Meta Language), langage qui supporte la modélisation des algorithmes distribués asynchrones, décrits en tant qu'automates non déterministes (SPIN signifie « Simple Promela Interpreter »). Les propriétés à vérifier sont exprimées sous forme de formules de logique temporelle linéaire (LTL), qui sont niées puis converties en automates de Büchi. En plus de sa fonction de vérificateur de modèles, SPIN peut également opérer comme simulateur, en suivant l'un chemin d'exécution possible à travers le système et en présentant la trace d'exécution résultante à l'utilisateur.
Contrairement à de nombreux vérificateurs de modèles, SPIN n'effectue pas lui-même la vérification de modèles, mais génère à la place des sources C pour un vérificateur de modèles spécifique adapté au problème. Cette technique économise de la mémoire et améliore les performances, tout en permettant également l'insertion directe de morceaux de code C dans le modèle. SPIN propose également un grand nombre d'options pour accélérer davantage le processus de vérification et économiser de la mémoire, telles que:
- réduction par ordre partiel ;
- compression d'états;
- hachage d'états par bits (en) (au lieu de stocker des états entiers, seul leur hash code est mémorisé dans un champ de bits; cela économise beaucoup de mémoire mais aux dépens de l'exhaustivité) ;
- faible exigence sur l'équité.
Historique
[modifier | modifier le code]Depuis 1995 environ, des ateliers SPIN annuels ont été organisés pour les utilisateurs SPIN, les chercheurs et les personnes généralement intéressées par la vérification de modèles . Le 26e workshop a eu lieu en 2019 à Pékin[3].
En 2001, l'Association for Computing Machinery a décerné à SPIN son Prix ACM Software System[4].
Voir aussi
[modifier | modifier le code]- NuSMV
- Uppaal Model Checker (en)
Références
[modifier | modifier le code]- « http://spinroot.com/spin/Doc/roots.html »
- « Release 6.5.2 », (consulté le )
- « 26th International SPIN Symposium on Model Checking of Software ».
- « Software System Award: ACM CITES TOOL TO DETECT SOFTWARE "BUGS" FOR PRESTIGIOUS AWARD. Bell Labs Researcher Developed "SPIN" to Make Computers More Reliable », ACM Press-Release.
Documentation
[modifier | modifier le code]- Gerard J. Holzmann, The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley, , 598 p. (ISBN 0-321-22862-6, lire en ligne).
- Samuel Hym, « SVL ― Introduction au Model-Checker Spin », Université de Lille, département informatique de la Faculté des Sciences et Technologies, (consulté le ).
- Balima Damien, « Spin model checker », Open Silicium, Open Silicium, no 9, (lire en ligne, consulté le ).
Liens externes
[modifier | modifier le code]
